As electronic devices of all kinds continue to proliferate, the demand for the integrated circuits or "chips" that operate the devices also continues to expand. New functionality and integration of more functionality onto smaller and smaller chips, makes it very difficult to verify new chip designs in a timely and comprehensive manner to insure that new designs operate in accordance with a design specification and design rules. As transistor devices become smaller, and more chip functionality is demanded, more transistor devices are included within new integrated circuits, and the verification process becomes so immense that for many newly designed integrated circuit models, verification is a critical bottleneck in the design flow.
The traditional approach of verification of digital systems is simulation: generating sequences of inputs to apply to the model under test, then verifying by hand or with a correctness checker whether the digital system behaved properly under the simulation run. While this methodology is simple, it is unfeasible to fully verify designs as their complexity increases since this would require an exponential amount of simulation time; the amount of simulation which can be performed in a timely manner yields lower and lower total coverage as logic complexity increases.
As a consequence of this simulation coverage problem, formal verification has become more and more popular. Formal verification is the process of rigorously verifying that an implementation of a logic design satisfies its specification. Note that the goal of simulation is the same, but that simulation is not rigorous. Model checking is a very popular form of formal verification.
In model checking, one of the most time consuming efforts is to provide a behavioral environment that "models" the microarchitectural interface to the unit under test. Traditionally, this effort can take several months, and being a manual effort, it is error prone. Consequently, verification may begin much later than is desired, and much time can be wasted by the verification engineers and the designers trying to weed through these "false fails" generated by an erroneous environment.
A digital design is composed of a collection of "state machines" that implement a required functionality. A "state machine" may be defined as an abstract machine consisting of a set of states, (including the initial state), a set of inputs, a set of outputs and a state transition function. The transition function takes the current state and an input and returns a new set of outputs and the next state. Since there is a one-to-one correspondence between "output values" and "states", only "states" will be referred to in the following discussion. A state machine can also be considered as a function which maps an ordered sequence of input events into a corresponding sequence of states.
The state of a sequential digital design at a given point in time is the cross product of the states of the various state machines in the design. This is hereinafter referred to as the "product state machine". A state transition table, which lists the transition from the current state to the next state for a given input, can then define the full functionality of such a sequential design. However, the verification of a sequential design requires not just the verification of the state transitions, but also all of the valid sequences of state transitions that can be traversed by the integrated circuit (IC) design being checked. A model checking tool can provide verification of all sequences of state transitions. A sequence of state transitions is hereinafter referred to as a "walk" or a "trace". The terms "walk" and "trace" are used interchangeably.
Accordingly, there is a need for an enhanced method for automating the generation of an environmental behavioral input required for model checking the designs of integrated circuits.